\pdfminorversion 7
\pdfobjcompresslevel 3

\documentclass[a4paper]{article}
\special{papersize=210mm,297mm}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{cite}
\usepackage[francais]{babel}
\usepackage[bookmarks=false,colorlinks,linkcolor=blue]{hyperref}
\usepackage[top=3cm,bottom=2cm,left=3cm,right=2cm]{geometry}
\usepackage{graphicx}
\usepackage{subfig}
\usepackage{eso-pic}
\usepackage{array}
\usepackage{color}
\usepackage{xcolor}
\usepackage{url}
\usepackage{listings}
\usepackage{url}
\usepackage{textcomp}
\usepackage{fancyhdr} 
\usepackage{multicol} 
\usepackage{proof} 
\usepackage{algpseudocode}
\usepackage{algorithm}

\definecolor{lightgray}{gray}{0.9}

\title{Rapport de TER, Master Informatique 1\up{ère} Année}
\author{David \textsc{DECLERCK} \& \\ Rémy \textsc{EL-SIBAIE BESOGNET}}


\newcommand{\HRule}{\rule{\linewidth}{0.5mm}}

\newcommand{\cub}{\texttt{cubicle}}
\newcommand{\alg}{\texttt{algony}}


\begin{document}


\input{./title.tex}

~
\vfill
\begin{center}
\section*{Résumé}
\end{center}

En informatique, la programmation concurrente est un paradigme qui
intéresse les scientifiques depuis des décénnies. En faisant l'état de
l'art on trouve de nombreux systèmes concurrents supposés sûrs qui
résolvent ce genre de problèmes. On peut citer plusieurs exemples :
l'algorithme de Szymanski, Peterson, etc.  Compte tenu de
l'utilisation critique de certains logiciels (aérospatiale, transports
en commun,\dots), on aimerait s'assurer que les systèmes évoqués
ci-dessus soient corrects. C'est là qu'intervient le principe du Model
Checking et plus précisément le logiciel \cub.

Durant notre TER, nous avons développé un compilateur d'un langage de
notre invention, \alg, vers le langage d'entrée de \cub. Ce
développement rend plus accessible ce Model Checker en permettant
d'écrire des algorithmes concurrents dans une sémantique plus proche
des langages impératifs auquel les programmeurs sont habitués.

\vfill

\newpage
\section*{Remerciements}

Nous remercions nos encadrants Sylvain Conchon et Alain Mebsout pour
le temps qu'ils nous ont consacré et leurs explications tout au long
de ce travail. Nous remercions aussi l'ensemble de l'équipe Toccata de
nous avoir accueilli en son sein deux jours par semaine pendant
plusieurs mois. Pour finir nous remercions David et Pierrick pour
l'accès à l'aquarium et le partage de la nourriture à poissons.

\newpage
\tableofcontents
%% \newpage
%% \listoffigures

\newpage
\section{Présentation}

\subsection{Le Model Checking}

De nos jours, de nombreux systèmes reposent sur des algorithmes
concurrents. On peut citer par exemple les protocoles de cohérence de
cache dans les microprocesseurs multi-coeurs. Une erreur dans un tel
protocole peut avoir des conséquences désastreuses, comme ce fut le
cas pour Intel avec le bug du processeur Pentium. Il est devenu
indispensable de vérifier que ces algorithmes soient corrects.

Le Model Checking consiste à \emph{prouver} qu'un algorithme présente
certaines propriétés, parmi les suivantes :
\begin{itemize}
\item sûreté (safety) : un état dangereux ne pourra jamais être atteint
\item vivacité (liveness) : quelque chose finira toujours par se produire
\item équité (fairness) : quelque chose pourra avoir lieu un nombre
infini de fois
\item absence d'interblocages (deadlocks) : un ou plusieurs processus
hors section critique ne doivent pas bloquer un ou plusieurs autres processus
\end{itemize}
On s'intéresse ici à la propriété de sureté. Par exemple, pour un
algorithme d'exclusion mutuelle, on veut s'assurer que deux processus
ne se retrouvent pas en même temps en section critique (c'est à dire,
qu'ils exécutent le même code au même moment).

\subsection{Approches pratiques}

Une première approche consiste à fixer le nombre de processus pour
lesquels on veut prouver les propriétés d'un algorithme donné. On a
donc un nombre fini de processus, et donc un nombre fini d'états. Il
suffit alors d'énumérer tous les états possibles, et de vérifier si
l'un d'entre eux correspond à un état dangereux. On
parle \emph{d'enumerated Model Checking}, ou encore de \emph{finite
state Model Checking}. De nombreux outils implémentant cette approche
existent. On peut citer notamment Mur$\varphi$, basé sur des
transitions, et Spin, qui utilise des automates.

Cependant, cette approche a la caractéristique d'être un problème de
complexité exponentielle en fonction du nombre de processus
. Dans la pratique, les outils reposant sur cette approche parviennent
à prouver des algorithmes pour 5 ou 6 processus au maximum.

Une autre approche a été utilisée pour prouver ces systèmes de manière
plus générale. L'idée est qu'au lieu de fixer le nombre de processus,
on considère qu'il en existe un nombre arbitrairement grand. La
complexité ne dépendra pas alors du nombre de processus puisqu'il est
quelconque. Malheureusement, l'indécidabilité de ce problème a été
démontrée par Apt et Kozen en 1986\cite{aptkozen}. Pour contourner
l'indécidabilité, on choisit un système limité, de sorte que la sûreté
de ce fragment soit démontrable. Les logiciels auxquels nous nous
intéressons utilisent les \emph{systèmes paramétrés à tableaux}. Ce
choix nous ramène à un problème décidable Sous certaines
conditions. Par exemple, MCMT est un Model Checker se basant sur cette
idée.

Mais celui qui nous intéresse vraiment est le logiciel
\cub\ \cite{conchon:hal-00778832}, développé au sein de l'équipe Toccata au
Laboratoire de Recherche en Informatique (LRI). \cub\ a été inspiré
par MCMT et permet de modéliser un système de transition comportant
un état initial et un ensemble d'états \emph{dangereux}. L'objectif
de \cub\ est de déterminer s'il existe un chemin entre l'état initial
et un des états dangereux. Pour répondre à cette question, il utilise
un algorithme d'atteignabilité arrière (on part des états dangereux et
on recherche les prédécesseurs, les \emph{pré-images}). C'est
une condition nécessaire pour rendre problème décidable. En
comparaison avec MCMT,
\cub\ implémente plusieurs fonctionnalités supplémentaires, telles que
la possibilité d'utiliser des types abstraits et énumérés, des
matrices, la possibilité de fixer le nombre de processus (On peut
citer le cas de l'algorithme de Peterson qui nécessite d'avoir deux
processus), un nombre non restreint de transitions, etc.  On peut
garantir la sûreté de \cub, ainsi que sa complétude dans quasiment
tout les cas. De même, sa terminaison est garantie sous plusieurs
conditions Pour finir, \cub\ possède un langage d'entrée qui permet
de définir l'état initial, les états dangereux, des variables
globales, et un ensemble de transitions. Il est basé sur le Model
Checker Mur$\varphi$.

\subsection{Problématique du TER}


Habituellement, nous rencontrons dans la littérature une
représentation impérative des algorithmes d'exclusion mutuelle, comme
le pseudo code C suivant qui correspond à l'algorithme de Peterson.

\label{peterson}
\begin{algorithm}[H]
\begin{verbatim}
// Variables partagées
int turn = 0;
bool flag[2] = {false};
//Code
flag[i] = true;
turn = j;
while (flag[j] && turn == j);
 // Section critique
flag[i] = false;
\end{verbatim}
\caption{Algorithme de Peterson en C}
\end{algorithm}

L'algorithme utilise deux variables, $flag$
et $turn$. Si $flag[n] = true $, alors le processus $n$ veut entrer
en section critique. La variable $turn$ conserve l'identifiant du
processus dont c'est le tour. L'entrée en section critique est
autorisée pour $p0$ si $p1$ ne veut pas entrer en section critique ou si
$p1$ a donné la priorité à $p0$ en passant $turn$ à 0


Le langage d'entrée de \cub\ est suffisement expressif pour permettre
de décrire un grand nombre d'algorithmes concurrents.  Cependant, la
représentation par un système de transitions qu'il emploie ne
correspond pas à aux méthodes présentées ci-dessus.  Traduire
manuellement ces algorithmes vers le langage de
\cub\ n'est donc pas une tâche triviale.
Il nous a donc été demandé de concevoir un langage de description
d'algorithmes plus impératif, et de traduire des algorithmes écrits
dans ce langage vers le langage d'entrée de \cub. Puis, nous avons
créé une interface permettant de suivre pas à pas l'exécution
d'algorithmes écrits dans notre langage à partir d'une trace menant à
un état dangereux. Il est à noter que le langage source n'est pas
conçu pour donner l'accès à toutes les fonctionnalités de \cub, mais
plutôt à un fragment. Notre but est limité à certains algorithmes,
et voir au delà est un travail plus conséquent.

\label{exemples}
Dans un premier temps, nous nous sommes interrogés sur les mécanismes
indispensables quand on écrit un algorithme concurrent d'exclusion
mutuelle. Par exemple, si on regarde le code de Peterson, on y utilise
des tableaux et c'est un des principes important du langage cible. On
observe aussi la présence d'une attente active que l'on doit
retrouver dans notre langage, ainsi que d'une section critique que nous
ferons apparaître explicitement. Le programme ci-dessous représente
l'algorithme de Szymanski dans un pseudo-langage algorithmique dont
nous nous sommes inspirés :

\begin{algorithm}
\begin{algorithmic}
\State $Bx\gets true$ \Comment{0}
\State \textbf{await} $\forall y$ . $x \neq y \Rightarrow not\
Sy$ \textbf{then} $Bx \gets false$ \Comment{1}
\State $Wx \gets true$; $Sx \gets true$; \Comment{2}

\If {$\exists y$ . $x \neq y \Rightarrow not\ By \wedge not\ Wy$} \Comment{3}
    \State $Sx \gets false$; $goto\ 4$
\Else
    \State $Wx \gets false$; $goto\ 5$
\EndIf
\State \textbf{await} $\exists y$ . $x \neq y \Rightarrow Sy \vee not\
Wx$ \textbf{then} $Wx \gets false$ ; $Sx \gets true$; \Comment{4}
\State \textbf{await} $\forall y$ . $x \neq y \Rightarrow not\ Wy$ \Comment{5}
\State \textbf{await} $\forall y$ . $y < y \Rightarrow not\ Sy$ \Comment{6}
\State \{Critical Section\} \Comment{7}
\State $Sx\gets false$; $goto\ 0$
\end{algorithmic}
\caption{Algorithme de Szymanski en pseudo-code algorithmique}
\end{algorithm}

Cet algorithme modélise une salle d'attente avec une porte de sortie
et une porte d'entrée. A l'état initial, la porte d'entrée est ouverte
et la porte de sortie est fermée. Tout les processus voulant accéder à la
section critique entrent dans la salle d'attente à peu près au même
moment. Les processus passent en section critique un par un, et le
dernier du groupe ferme la porte de sortie et réouvre la porte
d'entrée pour que le prochain groupe de processus puisse entrer. 

On retrouve le principe d'attente avec le mot clé \texttt{await},
ainsi qu'un système de sauts à base de \texttt{goto}, que nous
remplacerons par des boucles (afin de forcer les bonnes pratiques), et
bien évidemment une instruction conditionnelle. Il est intéressant de
noter dans cet exemple l'utilisation de quantificateurs, par ailleurs
présents dans \cub.

On observe également que l'instruction await est suivie d'un \texttt{then}
qui permet de d'effectuer de façon atomique les opérations qui la suivent.

\section{Langage source et langage cible}

\subsection{D'\alg...}

Nous nous sommes mis d'accord pour appeler notre outil et notre
langage \emph{\alg}\footnote{Provient des
mots \emph{Algorithm} et \emph{Tiny}, et il est proche du mot
anglais \emph{Agony}, qui pourrait représenter l'état d'une machine
qui doit prouver un système de transition conséquent via \cub.}. Si on
résume les points vus à la partie \ref{exemples}, il doit contenir les
fonctionnalités suivantes :
\begin{itemize}
\item des déclaration de variables, de tableaux
\item des déclations de types
\item des boucles
\item une instruction du type \emph{si-alors-sinon}
\item des quantificateurs universels et existentiels
\item une instruction d'attente
\item l'affectation de variables
\item une instruction pour effectuer des affectations atomiques
\end{itemize}

\subsubsection{Grammaire}
\begin{multicols}{2}\label{bnf}
\lstinputlisting{../bnf.txt}
\end{multicols}

Pour écrire la grammaire, nous nous sommes inspirés des
pseudo-langages rencontrés dans la littérature pour décrire des
algorithmes, tout en restant proches de \cub, pour une traduction plus
simple. Nous avons préféré limiter les symboles non-expressifs, tels
que les points virgules ou les accolades utilisées pour délimiter les
blocs. Un langage dont nous nous approchons serait Pascal. De fait,
l'analyseur syntaxique est assez restrictif. Ce dernier a subit de
très nombreuses évolutions au cours du développement. Effectivement,
si nous donnons trop de possibilités à l'utilisateur, la traduction
vers \cub\ n'en deviendra que plus ardue. Nous avons donc démarré avec
certains aprioris, et nous avons du nous remettre en question nos
choix au fur et à mesure que le développement progressait.



\subsubsection{Nos exemples}


\begin{algorithm}[H]
\begin{verbatim}
array B[proc] : bool 
array S[proc] : bool 
array W[proc] : bool 
current x 
while true do //L1
  B[x] := true  //L2
  await forall_other y . S[y] = false then atomic //L3
    B[x] := false 
    W[x] := true 
    S[x] := true 
  end
  if exists_other y . B[y] = false && W[y] = false then //L4
    S[x] := false //L5
    await exists_other y . S[y] = true && W[y] = false //L6
    atomic //L7
      W[x] := false 
      S[x] := true 
    end
  else
    W[x] := false //L8
  endif 
  await forall_other y . W[y] = false 
  await forall_other y . y >= x || S[y] = false 
  critical //Enter critical section
  S[x] := false 
done
\end{verbatim}
\caption{Algorithme de Szymanski en \alg}
\label{szymanski}
\end{algorithm}


\begin{algorithm}[H]
\begin{verbatim}
array Want[proc] : bool
var turn : proc
number_procs 2

process #1 : 
    while true do
          Want[#1] := true
          turn := #2
          await Want[#2] = false || turn = #1
          critical
          Want [#1] := false
    done
    
process #2 :
    while true do
          Want[#2] := true
          turn := #1
          await Want[#1] = false || turn = #2
          critical
          Want [#2] := false
    done
\end{verbatim}
\caption{Algorithme de Peterson en \alg}
\end{algorithm}
\subsection{... Vers \cub}
\label{cubicle}
Bien entendu, nous ne pouvons parler de traduction sans évoquer le
langage cible, à savoir celui de \cub. Notre but n'est pas ici de
donner une documentation complète sur \cub\ et son langage d'entrée,
mais uniquement d'introduire les concepts-clé dont nous avons besoin
pour notre traduction. Une partie des informations de cette section
sont extraites de l'article \emph{Vérification de systèmes paramétrés
avec \cub}\cite{conchon:hal-00778832}. Celui-ci se base sur un
système de transitions, où chacune est décrite par un couple garde /
actions, éventuellement paramétrée par un ou plusieurs identificateurs
de processus. Voyons un exemple de transition simple:

\begin{verbatim}
transition t (p1 p2)
requires { Tab[p1] = True && Tab[p2] = False && forall_other p3. (Tab[p3] = False) }
{
    Tab[p1] = False
    Tab[p2] = True
}
\end{verbatim}

Les paramètres de transition p1 et p2 sont des variables
existentiellement quantifiées représentant des identificateurs de
processus deux à deux distincts. La garde consiste en une conjonction
de littéraux et de formules universellement quantifiées. Ces formules
sont des disjonctions de conjonctions de littéraux, paramétrées par
une variable processus universellement quantifiée et distincte des
paramètres de la transition. Les actions sont des mises à jour de
variables ou de tableaux, réalisées de manière atomique. Par ailleurs,
l'état initial du système est décrit par une conjonction de littéraux
universellement quantifiés, représentant les valeurs initiales des
tableaux et variables qu'elle contient.

Un exemple d'état initial :
\begin{verbatim}
init (p) { Tab[p] = False && Var = 1 }
\end{verbatim}

Quant aux états dangereux, ils sont exprimés par des conjonctions de
littéraux quantifiés extistentiellement.

Un exemple d'état dangereux:
\begin{verbatim}
unsafe (p1 p2) { Tab[p1] = True && Tab[p2] = True }
\end{verbatim}

Concrètement, cet exemple définit comme dangereux un état où il existe
deux processus p1 et p2 distincts tels que la condition exprimée soit vraie.

\section{Le Langage \alg\ formalisé}

\subsection{Typage}

L'aspect restreint de notre langage \alg\ nous impose d'introduire
des jugements de typage particuliers.

\subsubsection{Expressions}

Afin de réaliser le typage des expressions, on introduit les jugements
suivants :
\begin{itemize}
\item $\Gamma \vdash e : \tau$ signifie que dans l'environnement $\Gamma$,
e est une expression bien typée de type $\tau$
\item $\Gamma \vdash_c e : \tau$ signifie que dans l'environnement $\Gamma$,
e est une constante bien typée de type $\tau$
\item $\Gamma \vdash_l e : \tau$ signifie que dans l'environnement $\Gamma$,
e est une valeur gauche bien typée de type $\tau$
\item $\Gamma \vdash_{at} e : \tau$ signifie que dans l'environnement $\Gamma$,
e est un terme atomique bien typé de type $\tau$
\item $\Gamma \vdash_t e : \tau$ signifie que dans l'environnement $\Gamma$,
e est un terme bien typé de type $\tau$
\item $\Gamma \vdash_q e : \tau$ signifie que dans l'environnement $\Gamma$,
e est une expression quantifiée bien typé de type $\tau$
\end{itemize}

On utilise également la notation $num(\tau)$ pour indiquer qu'un type
doit être numérique. Les types numériques sont les types $int$ et
$float$.

Les expressions les plus simples sont les constantes. Une constante
est bien typée si sa valeur correspond à une valeur permise pour son
type. Par ailleurs, si une constante est bien typée, alors c'est une
expression bien typée.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_c c : \tau}
      {c\ constante\ de\ type\ \tau}
&
\infer[]{\Gamma \vdash e : \tau}
      {\Gamma \vdash_c e : \tau}
\end{tabular}
\end{center}

Une expression limitée à une variable où à l'accès au contenu d'un
tableau est appelée une valeur gauche. Elles peuvent être utilisée à
gauche d'une affectation pour reçevoir une valeur. Ce sont également
des expressions bien typées.

\begin{center}
\begin{tabular}{ccc}
\infer[]{\Gamma \vdash_l x : \tau}
      {\tau\ x \in \Gamma & \tau \not\equiv \tau'[s_1, ..., s_n]}
&
\infer[]{\Gamma \vdash_l x[i_1, ..., i_n] : \tau}
      {\tau[s_1, ..., s_n]\ x \in \Gamma & \forall k, \Gamma \vdash i_k : proc}
&
\infer[]{\Gamma \vdash e : \tau}
      {\Gamma \vdash_l e : \tau}
\end{tabular}
\end{center}

L'ensemble des expressions constantes et des valeurs gauches constitue
ce que l'on appelle les termes atomiques. Les termes atomiques sont
des expressions bien typées.

\begin{center}
\begin{tabular}{ccc}
\infer[]{\Gamma \vdash_{ta} e : \tau}
      {\Gamma \vdash_c e : \tau}
&
\infer[]{\Gamma \vdash_{ta} e : \tau}
      {\Gamma \vdash_l e : \tau}
&
\infer[]{\Gamma \vdash e : \tau}
      {\Gamma \vdash_{ta} e : \tau}
\end{tabular}
\end{center}

Les opérations d'addition et de soustraction sont des expressions
particulières appelées termes. Ces opérations ne peuvent s'appliquer
qu'entre un terme atomique et une constante. Une constante ou une
valeur gauche seule sont également des termes. Un terme est une
expression bien typée.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_t e1\ op\ e2 : \tau}
      {\Gamma \vdash_{ta} e1 : \tau & \Gamma \vdash_c e2 : \tau &
      num(\tau) & op \in \{+, -\}}
&
\infer[]{\Gamma \vdash_t e2\ op\ e1 : \tau}
      {\Gamma \vdash_t e1\ op\ e2 : \tau}
\end{tabular}

\begin{tabular}{ccc}
\infer[]{\Gamma \vdash_t e : \tau}
      {\Gamma \vdash_c e : \tau}
&
\infer[]{\Gamma \vdash_t e : \tau}
      {\Gamma \vdash_l e : \tau}
&
\infer[]{\Gamma \vdash e : \tau}
      {\Gamma \vdash_t e : \tau}
\end{tabular}
\end{center}

Les opérations de comparaison sont des expressions produisant un
résultat de type $bool$. Tous les termes de type numériques peuvent être
comparés. Par ailleurs, les tests d'égalité et de différence sont
étendus aux termes de tout type.

\begin{center}
\begin{tabular}{c}
\infer[]{\Gamma \vdash e1\ op\ e2 : bool}
      {\Gamma \vdash_t e1 : \tau & \Gamma \vdash_t e2 : \tau &
      & num(\tau) & op \in \{>, <, <=, >=\}}
\end{tabular}

\begin{tabular}{c}
\infer[]{\Gamma \vdash e1\ op\ e2 : bool}
      {\Gamma \vdash_t e1 : \tau & \Gamma \vdash_t e2 : \tau &
      op \in \{=, <>\}}
\end{tabular}
\end{center}

Les opérateurs de conjonction et de disjonction acceptent comme
opérande toute expression de type $bool$, et produisent un résultat de
type $bool$.

\begin{center}
\begin{tabular}{c}
\infer[]{\Gamma \vdash e1\ op\ e2 : bool}
      {\Gamma \vdash e1 : bool & \Gamma \vdash e2 : bool &
      op \in \{\&\&, ||\}}
\end{tabular}
\end{center}

Enfin, les expressions universellement quantifiées sont un type
particulier d'expressions. Elles introduisent dans l'environnement une
variable de type $proc$, et vérifient une condition exprimée par une
expression de type $bool$. En raison des restrictions de notre
langage, elles ne sont pas incluses dans l'ensemble des expressions.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_q forall\_other\ x\ .\ e : bool}
      {\tau\ x \not\in \Gamma & \{proc\ x\} \cup \Gamma \vdash e : bool}
&
\infer[]{\Gamma \vdash_q exists\_other\ x\ .\ e : bool}
      {\tau\ x \not\in \Gamma & \{proc\ x\} \cup \Gamma \vdash e : bool}
\end{tabular}
\end{center}

\subsubsection{Instructions}

Pour réaliser le typage des instructions, on introduit les jugements
suivants :
\begin{itemize}
\item $\Gamma \vdash_i i$ signifie que dans l'environnement $\Gamma$,
i est une instruction bien typée
\item $\Gamma \vdash_a i$ signifie que dans l'environnement $\Gamma$,
i est une affectation bien typée
\item $\Gamma \vdash_{li} li$ signifie que dans l'environnement $\Gamma$,
li est une liste d'instructions bien typée
\item $\Gamma \vdash_{la} li$ signifie que dans l'environnement $\Gamma$,
li est une liste d'affectations bien typée
\end{itemize}

La plupart des instructions basées sur des expressions de type $bool$
existent en deux versions : une version avec quantificateur et une
version sans quantificateur. Ces instructions ont donc deux règles
d'inférence différentes.

Une affectation est une instruction prenant à gauche de l'opérateur
d'affectation une expression valeur gauche et à sa droite une
expression de même type. Une affectation bien typée est également une
instruction bien typée.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_a x\ :=\ e}
      {\Gamma \vdash_l x : \tau & \Gamma \vdash e : \tau}
&
\infer[]{\Gamma \vdash_i i}
      {\Gamma \vdash_a i}
\end{tabular}
\end{center}

L'instruction d'entrée en section critique est une instruction
toujours bien typée.

\begin{center}
\begin{tabular}{c}
\infer[]{\Gamma \vdash_i critical}
      {}
\end{tabular}
\end{center}

L'instruction d'assertion est bien typée si l'expression à
vérifier est bien typée de type $bool$.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_i assert\ e}
      {\Gamma \vdash e}
&
\infer[]{\Gamma \vdash_i assert\ e}
      {\Gamma \vdash_q e}
\end{tabular}
\end{center}

L'instruction conditionnelle est bien typée si l'expression utilisée
comme condition est bien typée de type $bool$, et si les listes
d'instructions qu'elle emploie sont bien typées.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_i if\ e\ then\ li1\ else\ li2\ endif}
      {\Gamma \vdash e : bool & \Gamma \vdash_{li} li1 & \Gamma \vdash_{li} li2}
&
\infer[]{\Gamma \vdash_s if\ e\ then\ li1\ else\ li2\ endif}
      {\Gamma \vdash_q e : bool & \Gamma \vdash_{li} li1 & \Gamma \vdash_{li} li2}
\end{tabular}
\end{center}

La boucle tant que est bien typée si l'expression utilisée
comme condition est bien typée de type $bool$, et si la liste
d'instruction qu'elle emploie est bien typées.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_i while\ e\ do\ li\ done}
      {\Gamma \vdash e : bool & \Gamma \vdash_{li} li}
&
\infer[]{\Gamma \vdash_i while\ e\ do\ li\ done}
      {\Gamma \vdash_q e : bool & \Gamma \vdash_{li} li}
\end{tabular}
\end{center}

L'instruction d'attente est bien typée si l'expression sur laquelle
elle repose est bien typée de type $bool$, et si l'instruction à
exécuter de façon atomique est également bien typée.

\begin{center}
\begin{tabular}{c}
\infer[]{\Gamma \vdash_i await\ e\ then\ i}
      {\Gamma \vdash_q e : bool & \Gamma \vdash_i i}
\end{tabular}
\end{center}

Un bloc d'instructions atomique est bien typé si la liste des
instructions qu'il contient est une liste d'affectations bien typée.

\begin{center}
\begin{tabular}{c}
\infer[]{\Gamma \vdash_i atomic\ li\ endatom}
      {\Gamma \vdash_{la} li}
\end{tabular}
\end{center}

Une liste d'affectations est bien typée si chacune des affectations qui
la compose est une affectation bien typée. Une telle liste est
également une liste d'instructions bien typée.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_{la} i_1\ ...\ i_n}
      {\forall k \leq n, \Gamma \vdash_a i_k}
&
\infer[]{\Gamma \vdash_{li} i_1\ ...\ i_n}
      {\Gamma \vdash_{la} i_1\ ...\ i_n}
\end{tabular}
\end{center}

Une liste d'instructions est bien typée si chacune des instructions qui
la compose est bien typée.

\begin{center}
\begin{tabular}{cc}
\infer[]{\Gamma \vdash_{li} i_1\ ...\ i_n}
      {\forall k \leq n, \Gamma \vdash_i i_k}
\end{tabular}

\end{center}

\subsection{Sémantique par traduction}

Nous avons choisi de représenter la sémantique de notre langage en
donnant, pour chaque instruction, la traduction typique dans le
langage de \cub.

Ce langage étant basé sur des transitions, nous avons introduit une
variable paramétrée PC, qui représente pour chaque processus le numéro
de l'instruction sur laquelle il se trouve. Ainsi, toutes les
transitions testent la valeur de cette variable dans leur garde, et la
modifient dans leur actions, ce qui permet d'assurer un ordre
d'exécution précis. Les numéros des instructions sont représentés par un type
énuméré location.

\subsubsection{Nombre de processus}

Nous avons vu en introduction que \cub\ traitait un nombre arbitraire
de processus, mais que certains algorithmes ne s'écrivaient qu'avec un
nombre fixé de processus, comme Peterson \ref{peterson}. Evidemment,
si le nombre de processus est arbitraire, le code est dupliqué. Mais
imaginons que l'algorithme décrive des processus possédant des
executions différentes ? \cub\ implémente cette possibilité en fixant
en en-tête du code le nombre de processus. On fait référence ensuite à
ces derniers via leurs identifiants $\#1, \#2,\dots, \#k$. On peut
écrire plusieurs blocs correspondant au code de chaque
processus. Nous avons ajouté cette fonctionnalité dans le
langage \alg\, qui se traduit directement dans \cub.

\begin{verbatim}
number_procs 2
\end{verbatim}

On peut rester en mode $n$ processus en désignant le nom du processus
courant :

\begin{verbatim}
current x
\end{verbatim}

Il faut ensuite traiter différemment les différentes instructions en
fonction du mode. La différence majeure est que l'on retire les
paramètres des transitions en mode \emph{fixé} (effectivement, le
processus concerné est directement nommé).


\subsubsection{Affectation simple}

L'affectation simple consiste à placer dans une variable (paramétrée
ou non) le résultat d'une expression simple (constante littérale,
contenu d'une variable ou addition / soustraction d'une variable et
d'une constante littérale).
Nous avons traduit les affectations simples par une unique transition,
comprenant uniquement l'affectation.

%% | <leftval> assign <term> ;

\begin{verbatim}
(* Gestion des numéros d'instruction *)
type location = L1 | L2
array PC [proc] : location

(* Etat initial : instruction L1 *)
init (p) { PC[p] = L1 }

(* Transition : effectuer l'affectation *)
transition assign (p)
requires { PC[p] = L1 }
{
    <leftval> := <term>
    PC[p] = L2
}
\end{verbatim}


\subsubsection{Bloc d'affectations atomique}

Un bloc d'affectations atomique permet de réaliser plusieurs
affectations simples de façon atomique, ce qui se traduit sous \cub\
par une unique transition qui regroupe toutes les affectations du bloc
atomique.

%% | atomic <stmts> endatom ;

\begin{verbatim}
(* Gestion des numéros d'instruction *)
type location = L1 | L2
array PC [proc] : location

(* Etat initial : instruction L1 *)
init (p) { PC[p] = L1 }

(* Transition : effectuer les affectations de façon atomique *)
transition atomic (p)
requires { PC[p] = L1 }
{
    (<leftval> := <term>)*
    PC[p] = L2
}

\end{verbatim}


\subsubsection{Section critique}

Cette instruction permet de vérifier de façon simple que deux
processus ne se retrouvent pas en même temps au même point
d'exécution. Nous la traduisons par une formule unsafe sous \cub,
ainsi que par une transition fantôme (permettant simplement de situer
l'instruction).

%% | critical ;

\begin{verbatim}
(* Gestion des numéros d'instruction *)
type location = L1 | L2
array PC [proc] : location

(* Etat initial : instruction L1 *)
init (p) { PC[p] = L1 }

(* Transition : passer à l'instruction suivante *)
transition crit (p)
requires { PC[p] = L1 }
{
    PC[p] = L2
}

(* Etat dangereux : atteint si p1 et p2 sont tous les deux sur L1 *)
unsafe (p1 p2) { PC[p1] = L1 && PC[p2] = L1 }
\end{verbatim}

\subsubsection{Assertion}

Les assertions permettent de vérifier qu'une condition soit vérifiée
en un point donné du programme. Nous les traduisons par des formules
unsafe sous \cub.

%% | assert <qterm> ;

\begin{verbatim}
(* Gestion des numéros d'instruction *)
type location = L1 | L2
array PC [proc] : location

(* Etat initial : instruction L1 *)
init (p) { PC[p] = L1 }

(* Etat dangereux : atteint si instruction L1 et condition vraie *)
unsafe (p) { PC[p] = L1 && <qterm> }
\end{verbatim}

\subsubsection{Boucle tant que}

Les boucles tant que permettent de répéter un bloc d'instructions tant
qu'une condition est vérifiée. Cette condition peut être une
expression booléenne, ou une formule universellement quantifiée. Nous
les avons traduites par un ensemble de plusieurs transitions,
représentant les différentes étapes de la boucle.

%% | while <qterm> do <stmts> done ;

\begin{verbatim}
(* Gestion des numéros d'instruction *)
type location = L1 | L2 | L3
array PC [proc] : location

(* Etat initial : instruction L1 *)
init (p) { PC[p] = L1 }

(* Transition : si le test du while est vrai, passer à L2 *)
transition while_true (p)
requires { PC[p] = L1 && <qterm> }
{
    PC[p] = L2
}

(* Transition(s) : instruction(s) a exécuter dans le while, *)
(* puis repasser à L1 pour réévaluer la condition du while *)
transition stmts (p)
requires { PC[p] = L2 }
{
    <stmts>
    PC[p] = L1
}

(* Transition : si le test du while est faux, passer à L3 *)
transition while_false (p)
requires { PC[p] = L1 && !<qterm> }
{
    PC[p] = L3
}
\end{verbatim}

\subsubsection{Instruction conditionnelle}

L'instruction conditionnelle permet d'exécuter un bloc d'instruction
si une condition est vérifiée, et un autre bloc si elle ne l'est pas.
Cette condition peut être une expression booléenne, ou une formule
universellement quantifiée. Nous les avons traduites par un ensemble
de plusieurs transitions, représentant les différents cas.

%% | if <qterm> then <stmts> endif ;
%% | if <qterm> then <stmts> else <stmts> endif ;
\begin{verbatim}
if <qterm> then (* L1 *)
  <stmts> (* L2 *)
else
  <stmts> (* L3 *)
endif
(* L4 *)
  
\end{verbatim}

Ce code se traduit de la façon suivante en \cub\ : 

\begin{verbatim}
type location = L1 | L2 | L3 | L4
array PC [proc] : location
init (p) { PC[p] = L1 }

(* Si la garde du if est vraie, on passe à la localisation suivante *)
transition if_true (p)
requires { PC[p] = L1 && <qterm> }
{
    PC[p] = L2
}

(* On effectue le corps du if et on saute le else ensuite *)
transition true_stmts (p)
requires { PC[p] = L2 }
{
    <stmts>
    PC[p] = L4
}

(* Si la garde du if est fausse, on saute les transitions qui
correspondent au corps du if et on passe au contenu du else *)
transition if_false (p)
requires { PC[p] = L1 && !<qterm> }
{
    PC[p] = L3
}

(* On effectue le corps du else et on passe à la suite *)
transition false_stmts (p)
requires { PC[p] = L3 }
{
    <stmts>
    PC[p] = L4
}
\end{verbatim}


\subsubsection{Barrière de synchronisation}

Une barrière de synchronisation bloque l'exécution tant qu'une
condition n'est pas vérifiée. Une fois la condition vérifiée,
un ensemble (optionnel) d'instructions (limitées à des affectations)
peut être exécuté de façon atomique. Nous avons traduit ces
barrières de synchronisation par une unique transition.

%% | await <quantifier> (then <stmt>)|;

\begin{verbatim}
(* Gestion des numéros d'instruction *)
type location = L1 | L2
array PC [proc] : location

(* Etat initial : instruction L1 *)
init (p) { PC[p] = L1 }

(* Transition : si la condition est vraie, exécuter l'instruction *)
transition await (p)
requires { PC[p] = L1 && <qterm> }
{
    (<leftval> := <term>)*
    PC[p] = L2
}
\end{verbatim}

\subsubsection{Les formules logiques}

Dans \alg, nous utilisons des formules logiques dans différentes
instructions. Ces formules peuvent avoir n'importe quelle forme, de
par l'utilisation des opérateurs logiques \emph{et}, \emph{ou} et de
comparaison. Ces formules, après traduction seront répercutées sur les
gardes des transitions correspondant aux
instructions. Malheureusement, les gardes de \cub\ ne peuvent contenir
que des conjonctions de littéraux\footnote{Littéraux séparées par
l'opérateur \emph{et}. e.g.\ $a \wedge b$,...}  ou des formes normales
disjonctives (FND\footnote{Conjonctions de littéraux séparées par
l'opérateur \emph{ou}. e.g.\ $a \wedge b \vee c \wedge b$,...})
universellement quantifiées.  Si l'on veut représenter une FND sans
quantificateur universel, on est obligé de la diviser en autant de
transitions qu'il y a de conjonctions. Concrètement, la satisfiabilité
d'une conjonction, équivaut pour \cub\ à la possibilité de choisir la
transition comportant cette conjonction dans la garde.

\begin{verbatim}
if (a || b) && (c || d) then
  (* do something *)
endif
\end{verbatim}

Evidemment, dans une étape préliminaire, nous devons transformer la
formule en FND pour ensuite la diviser.  Ce problème a une compléxité
quadratique en la taille de la formule.  Dans notre exemple on obtient
: $(a \wedge b) \vee (a \wedge d) \vee (b \wedge c) \vee (b \wedge
d)$, ce qui fait quatre conjonctions, qui vont correspondre à quatre
transitions. Ensuite l'instruction \texttt{if} va génerer trois
transitions (pas de \texttt{else}) par conjonction. On obtient donc
douze transitions générées pour traduire cette instruction.

\subsubsection{Les quantificateurs}

Dans \alg, nous nous sommes pliés aux règles du langage cible en
ajoutant les quantificateurs \emph{Il existe un autre} et \emph{Pour
tout autre}. Ce \emph{autre} signifie implicitement \emph{autre que le
processus courant}. Il est indispensable de laisser cette précision
car c'est la seule manière d'utiliser des variables quantifiées
sous \cub.  Le \texttt{forall\_other} de \alg\ correspond rigoureusement
à celui de \cub. Par contre, le \texttt{exists\_other} nécessite une
traduction plus subtile :

\begin{verbatim}
if exists_other y . Tab[y] = true && Tab[x] = true then
   ... (* do something *)
endif
\end{verbatim}
Dans cet exemple, on va générer un \texttt{if} comme expliqué
précédemment, sauf que les transitions qui comporteront dans leur
garde la formule logique ci-dessus (qui ne sera pas quantifiée
explicitement) se verront ajouter un processus en paramètre, qui sera
ce processus \texttt{y}. De fait, dans \cub, les processus en
paramètre des transitions sont implicitement différents et
existentiellement quantifiés, ce qui est tout à fait la sémantique de
notre \texttt{exists\_other}.

On notera qu'il n'y a la possibilité de quantifier qu'une seule
variable sous \alg\ (donc pas de quantificateurs imbriqués), et la
possibilité de ne mettre qu'un seul quantificateur par formule
logique. Il y a plusieurs raisons à celà. Premièrement, si on imbrique
plusieurs existentiels, en logique classique, rien ne dit que ces
variables doivent être différentes les unes des autres (même sous la
forme \texttt{exists\_other}). Sous \cub\ par contre, les processus en
paramètre d'une transition sont explicitement distincts deux à
deux. Nous aurions eu une incohérence de sémantique au moment de la
traduction, d'autant plus que celle ci ne serait pas apparue sur
le \texttt{forall\_other}. On aurait donc également eu une incohérence
entre les deux quantificateurs. Il est malheureux de constater que
nous bridons volontairement \cub, mais le but était d'avoir un fragment
fonctionnel, et cette partie aurait nécessité plus de réflexion.

\section{Outil graphique de suivi de trace}

\subsection{Le besoin}

Lorsque \cub\ détecte qu'un état dangereux est atteignable, il génère
une trace d'exécution menant à cet état, en mentionnant toutes les
transitions prises. On veut pouvoir faire le lien entre cette trace et
le code correspondant sous \alg. De plus, on veut pouvoir simuler
l'exécution pas à pas de cette trace pour chaque processus présent
dans la trace, dans le but d'aider l'utilisateur à trouver l'origine
du problème, et à comprendre comment son programme en arrive à être
dangereux.

\subsection{Réalisation}

Nous avons utilisé GTK, par le biais de la librairie LablGTK, et le
contrôle GtkSourceView2, pour réaliser une petite interface graphique
répondant au besoin. La principale subtilité a consisté à faire le
lien entre les transitions du code \cub\ et les numéros de ligne du
code \alg. Nous avons pour cela modifié notre compilateur de façon à
intégrer dans le nom de chaque transition \cub\ générée le numéro de
la ligne correspondante dans le code source \alg. Ainsi, la trace
contient toutes les informations nécessaires à sa simulation.

\subsection{Présentation de l'application}

Le code source du programme \alg\ est affiché en autant d'exemplaires
que nécessaire, et la ligne d'éxécution courante est surlignée. Un
bouton permet de dérouler l'exécution pas à pas, jusqu'à atteindre
l'état unsafe. Un autre permet de reprendre l'exécution au début.  En
guise d'exemple nous avons modifié l'algorithme de Szymanski.  Dans
l'instruction 3, on nous avons retiré l'instruction \texttt{atomic}
qui permet d'effectuer les affectations suivantes atomiquement.


\begin{algorithm}[H]
\begin{verbatim}
array B[proc] : bool
array S[proc] : bool
array W[proc] : bool
current x
while true do // L1
  B[x] := true // L2
  await forall_other y . S[y] = false //L3 : On retire l'instruction atomic
  B[x] := false
  W[x] := true
  S[x] := true
  if exists_other y . B[y] = false && W[y] = false then // L4
    S[x] := false // L5
    await exists_other y . S[y] = true && W[y] = false // L6
    atomic // L7
      W[x] := false
      S[x] := true
    end
  else
    W[x] := false // L8
  endif
  await forall_other y . W[y] = false
  await forall_other y . y >= x || S[y] = false
  critical // Enter critical
  section S[x] := false
done
\end{verbatim}
\caption{Algorithme de Szymanski Dangereux}
\end{algorithm}


\begin{figure}[H]
   \centering
   \includegraphics[scale=0.4,bb=0 0 1131 487]{gui_green.png}
   \caption{Déroulement d'une trace}
   \label{img_deroulement}
\end{figure}

\begin{figure}[H]
   \centering
   \includegraphics[scale=0.4,bb=0 0 1131 487]{gui_crit.png}
   \caption{Les deux processus sont en même temps en section critique}
   \label{img_critique}
\end{figure}

Sur la figure \ref{img_critique}, on peut observer le résultat de
l'exécution de la trace dangereuse. En temps normal la sûreté de cet
algorithme repose sur le fait que l'instruction 3 exécute
l'affectation $B[x] = false$ de façon atomique après la barrière de
synchronisation. Les deux processus se retrouvent donc tous les deux
en section critique.

\section{Perspectives d'évolution}

Bien que notre outil produise le résultat attendu, la compilation ne
donne pas forcément un code \cub\ parfaitement optimisé, et certaines
fonctionnalités du langage cible restent inaccessibles depuis \alg\
(comme la mise à jour de tableaux par exemple, ou la quantification de
plusieurs variables). De plus, il aurait été très intéressant
d'intégrer directement une partie de notre travail au logiciel \cub,
afin de donner plus d'informations à l'utilisateur durant l'affichage
de la trace. Sans aller jusque là, au moins trois possibilités
d'évolution sont envisageables.

\subsection{Détection des interblocages}

Nous avons vu en introduction que la propriété de sûreté, sur laquelle
nous avons travaillé ici, n'était pas la seule que nous souhaitions
prouver. Nous pouvons envisager d'étendre notre langage pour détecter
les interblocages.

Un interblocage se produit lorsqu'au moins deux processus s'attendent
mutuellement, c'est à dire, attendent chacun qu'une ressource prise
par l'autre processus soit libérée afin de pouvoir continuer leur
exécution. Les deux processus étant bloqués, il n'y a plus aucune
chance pour que la ressource nécessaire à l'autre soit libérée. La
situation est donc inextricable.

Concrètement, sous \cub, atteindre ce type de situation dangereuse revient à
dire qu'aucune transition ne peut être prise. Il faut donc générer une
formule unsafe traduisant cet état de fait. La formule en question
correspond en fait à la négation de la disjonction de toutes les
gardes des transitions, ou, autrement dit, à la conjonction des
négations des gardes de toutes les transitions. Il peut donc en
résulter un grand nombre de formules unsafe.

Prenons un exemple simple de transitions exhibant un interblocage :
\begin{verbatim}
transition t1 (x)
requires { T[x] = true }
{
    U[x] := true;
}

transition t2 (x)
requires { U[x] = true }
{
    T[x] := true;
}
\end{verbatim}

Cet exemple repose sur les suppositions suivantes :
\begin{itemize}
\item $T[x] = false$ et $U[x] = false$ pour tout processus x
\item cet état est atteignable (il existe d'autres transitions
pouvant y mener)
\item aucune autre transition ne peut être prise
\end{itemize}

Ici, on voit clairement que des processus attendent que $T[x] = true$
pour mettre $U[x]$ à $true$, et que des processus attendent que $U[x]
= true$ pour mettre $T[x]$ à $true$. Or, ces conditions sont
mutuellement exclusives et ne peuvent donc être en même temps
satisfaites.

Pour détecter cet interblocage, il faut écrire la formule unsafe
correspondant à la négation des gardes de t1 et t2. Si l'on fait
abstraction des autres transitions (il faudrait normalement les
prendre en compte), notre formule unsafe devrait exprimer la condition suivante:

\begin{verbatim}
unsafe (x) { T[x] = false && forall_others y . T[y] = false &&
             U[x] = false && forall_others y . U[y] = false }
\end{verbatim}


\subsection{Exécution de code \alg\ par un interpréteur}

En l'état actuel des choses, notre outil graphique ne permet que de
dérouler une trace d'exécution menant à un état non sûr. Il ne permet
notamment pas de suivre l'état des variables, ce qui rend difficile la
recherche de la cause de l'erreur. Nous pouvons aisément imaginer
écrire un interpréteur pour notre langage \alg, qui permettrait de
simuler l'évolution des variables au cours du temps. Il s'agirait
toujours de suivre une trace d'exécution menant à un état unsafe, mais
en même temps, de répercuter les instructions d'affectation sur une
structure interne destinée à stocker l'état des variables.


\subsection{Prouver la correction de la traduction}

Bien que nous ayons donné la sémantique de notre langage en donnant
pour chaque construction sa traduction dans le langage de \cub, nous
n'avons pas prouvé que notre traduction était correcte. Le langage
étant assez restreint, et les constructions étant simples à exprimer,
on peut donner l'intuition que notre langage est effectivement correct
(bien que cela ne reste qu'une supposition). Si le langage s'avérait
être plus complexe, nous ne pourrions plus donner cette intuition, et
il faudrait en réaliser la preuve.

\newpage
\section{Conclusion}

L'objectif de ce TER était de réaliser un projet qui réponde à des
problématiques de recherche sur lesquels nous avons réfléchi au
préalable, via la littérature. Plus précisément, le but était de
concevoir et réaliser le compilateur d'un langage de notre invention
vers le langage d'entrée du Model Checker \cub. Les résultats sont
concluants puisqu'il est dorénavant possible d'écrire des algorithmes
tels que Szymanski ou Peterson dans le langage \alg, et de prouver
ensuite qu'ils sont sûrs via \cub. Sans l'avoir démontré, nous avons
constaté que la traduction vers \cub\ était sémantiquement correcte.
De plus, nous avons ajouté une interface très réduite qui permet de
visualiser dans le code source \alg\ la trace du programme envoyé
à \cub\ pour arriver à un état dangereux.

En conclusion, il a été très agréable pour nous de travailler et
d'apprendre auprès de chercheurs du LRI, notemment Sylvain Conchon.
De plus, nous avons été familiarisés avec la discipline de la preuve de
programmes, et plus particulièrement avec les méthodes de Model
Checking, qui nous étaient jusqu'alors inconnues.

\newpage
\addcontentsline{toc}{section}{\protect\numberline{}Bibliographie}
\bibliographystyle{plain}
\bibliography{./biblio}




\end{document}


# Local Variables:
# compile-command: "rubber -d --inplace rapport.tex"
# End:

